%include
:- lib(ic), lib(listut).

testTriangleCategory(Path, OState, Arg, Result, NState) :-
	Path > 0,
	% Domains
	[OSideA] :: -127 .. 128,
	[NSideA] :: -127 .. 128,
	[OSideB] :: -127 .. 128,
	[NSideB] :: -127 .. 128,
	[OSideC] :: -127 .. 128,
	[NSideC] :: -127 .. 128,
	% Constraints
	OState = [OSideA, OSideB, OSideC],
	NState = [NSideA, NSideB, NSideC],
	triangleCategory(Path, OState, Arg, Result, NState),
	% Solving
	indomain(OSideA),
	indomain(NSideA),
	indomain(OSideB),
	indomain(NSideB),
	indomain(OSideC),
	indomain(NSideC).

triangleCategory(1, [OSideA, OSideB, OSideC], [], Result, [NSideA, NSideB, NSideC]) :-
	% Invariant
	OSideA + OSideB #> OSideC,
	OSideB + OSideC #> OSideA,
	OSideA + OSideC #> OSideB,
	% Postcondition
	neg(OSideA #= OSideB),
	neg(OSideA #= OSideC),
	neg(OSideB #= OSideC),
	Result = 'Scalene',
	NSideA #= OSideA,
	NSideB #= OSideB,
	NSideC #= OSideC,
	% Object State Update
	NSideA #= OSideA,
	NSideB #= OSideB,
	NSideC #= OSideC,
	% Invariant
	NSideA + NSideB #> NSideC,
	NSideB + NSideC #> NSideA,
	NSideA + NSideC #> NSideB.

